Issue4638-3.agda:9,7-8
Identifier c is declared erased, so it cannot be used here
when checking that the expression c has type D
